<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link href="common/css/sf.css" rel="stylesheet" type="text/css" />
<title>Typechecking: A Typechecker for STLC</title>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/plf.css" rel="stylesheet" type="text/css"/>
</head>

<body>

<div id="page">

<div id="header">
<div id='logoinheader'><a href='https://softwarefoundations.cis.upenn.edu'>
<img src='common/media/image/sf_logo_sm.png' alt='Software Foundations Logo'></a></div>
<div class='booktitleinheader'><a href='index.html'>Volume 2: Programming Language Foundations</a></div>
<ul id='menu'>
   <li class='section_name'><a href='toc.html'>Table of Contents</a></li>
   <li class='section_name'><a href='coqindex.html'>Index</a></li>
   <li class='section_name'><a href='deps.html'>Roadmap</a></li>
</ul>
</div>

<div id="main">

<h1 class="libtitle">Typechecking<span class="subtitle">A Typechecker for STLC</span></h1>


<div class="doc">

<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" title="var">has_type</span></span> relation of the STLC defines what it means for a
    term to belong to a type (in some context).  But it doesn't, by
    itself, give us an algorithm for <i>checking</i> whether or not a term
    is well typed.

<div class="paragraph"> </div>

    Fortunately, the rules defining <span class="inlinecode"><span class="id" title="var">has_type</span></span> are <i>syntax directed</i>
    -- that is, for every syntactic form of the language, there is
    just one rule that can be used to give a type to terms of that
    form.  This makes it straightforward to translate the typing rules
    into clauses of a typechecking <i>function</i> that takes a term and a
    context and either returns the term's type or else signals that
    the term is not typable.  
<div class="paragraph"> </div>

 This short chapter constructs such a function and proves it
    correct. 
</div>
<div class="code">

<span class="id" title="keyword">Set</span> <span class="id" title="var">Warnings</span> "-notation-overridden,-parsing,-deprecated-hint-without-locality".<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Coq</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Bool.Bool.html#"><span class="id" title="library">Bool.Bool</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="library">Maps</span>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Smallstep.html#"><span class="id" title="library">Smallstep</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Stlc.html#"><span class="id" title="library">Stlc</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">PLF</span> <span class="id" title="keyword">Require</span> <a class="idref" href="MoreStlc.html#"><span class="id" title="library">MoreStlc</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Module</span> <a id="STLCTypes" class="idref" href="#STLCTypes"><span class="id" title="module">STLCTypes</span></a>.<br/>
<span class="id" title="keyword">Export</span> <span class="id" title="var">STLC</span>.<br/>
</div>

<div class="doc">
<a id="lab358"></a><h1 class="section">Comparing Types</h1>

<div class="paragraph"> </div>

 First, we need a function to compare two types for equality... 
</div>
<div class="code">

<span class="id" title="keyword">Locate</span> "Bool".<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Fixpoint</span> <a id="STLCTypes.eqb_ty" class="idref" href="#STLCTypes.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> (<a id="T<sub>1</sub>:1" class="idref" href="#T<sub>1</sub>:1"><span class="id" title="binder">T<sub>1</sub></span></a> <a id="T<sub>2</sub>:2" class="idref" href="#T<sub>2</sub>:2"><span class="id" title="binder">T<sub>2</sub></span></a>:<a class="idref" href="Stlc.html#STLC.ty"><span class="id" title="inductive">ty</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#T<sub>1</sub>:1"><span class="id" title="variable">T<sub>1</sub></span></a>,<a class="idref" href="Typechecking.html#T<sub>2</sub>:2"><span class="id" title="variable">T<sub>2</sub></span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> , <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#STLC.:::'true'"><span class="id" title="notation">true</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a> <span class="id" title="var">T<sub>11</sub></span><a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a><span class="id" title="var">T<sub>12</sub></span> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>, <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a> <span class="id" title="var">T<sub>21</sub></span><a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a><span class="id" title="var">T<sub>22</sub></span> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#andb"><span class="id" title="definition">andb</span></a> (<a class="idref" href="Typechecking.html#eqb_ty:3"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>11</sub></span> <span class="id" title="var">T<sub>21</sub></span>) (<a class="idref" href="Typechecking.html#eqb_ty:3"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>12</sub></span> <span class="id" title="var">T<sub>22</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" title="var">_</span>,<span class="id" title="var">_</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Stlc.html#STLC.:::'false'"><span class="id" title="notation">false</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
... and we need to establish the usual two-way connection between
    the boolean result returned by <span class="inlinecode"><span class="id" title="var">eqb_ty</span></span> and the logical
    proposition that its inputs are equal. 
</div>
<div class="code">

<span class="id" title="keyword">Lemma</span> <a id="STLCTypes.eqb_ty_refl" class="idref" href="#STLCTypes.eqb_ty_refl"><span class="id" title="lemma">eqb_ty_refl</span></a> : <span class="id" title="keyword">∀</span> <a id="T:6" class="idref" href="#T:6"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Typechecking.html#STLCTypes.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> <a class="idref" href="Typechecking.html#T:6"><span class="id" title="variable">T</span></a> <a class="idref" href="Typechecking.html#T:6"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Stlc.html#STLC.:::'true'"><span class="id" title="notation">true</span></a>.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">T</span>. <span class="id" title="tactic">induction</span> <span class="id" title="var">T</span>; <span class="id" title="tactic">simpl</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHT1</span>. <span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHT2</span>. <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" title="keyword">Lemma</span> <a id="STLCTypes.eqb_ty__eq" class="idref" href="#STLCTypes.eqb_ty__eq"><span class="id" title="lemma">eqb_ty__eq</span></a> : <span class="id" title="keyword">∀</span> <a id="T<sub>1</sub>:7" class="idref" href="#T<sub>1</sub>:7"><span class="id" title="binder">T<sub>1</sub></span></a> <a id="T<sub>2</sub>:8" class="idref" href="#T<sub>2</sub>:8"><span class="id" title="binder">T<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Typechecking.html#STLCTypes.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> <a class="idref" href="Typechecking.html#T<sub>1</sub>:7"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="Typechecking.html#T<sub>2</sub>:8"><span class="id" title="variable">T<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Stlc.html#STLC.:::'true'"><span class="id" title="notation">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Typechecking.html#T<sub>1</sub>:7"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Typechecking.html#T<sub>2</sub>:8"><span class="id" title="variable">T<sub>2</sub></span></a>.<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">T<sub>1</sub></span>. <span class="id" title="tactic">induction</span> <span class="id" title="var">T<sub>1</sub></span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">T<sub>2</sub></span> <span class="id" title="var">Hbeq</span>; <span class="id" title="tactic">destruct</span> <span class="id" title="var">T<sub>2</sub></span>; <span class="id" title="tactic">inversion</span> <span class="id" title="var">Hbeq</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T<sub>1</sub>=Bool&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T<sub>1</sub>&nbsp;=&nbsp;T1_1<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>T1_2&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Bool.Bool.html#andb_true_iff"><span class="id" title="lemma">andb_true_iff</span></a> <span class="id" title="keyword">in</span> <span class="id" title="var">H<sub>0</sub></span>. <span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>0</sub></span> <span class="id" title="keyword">as</span> [<span class="id" title="var">Hbeq1</span> <span class="id" title="var">Hbeq2</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">IHT1_1</span> <span class="id" title="keyword">in</span> <span class="id" title="var">Hbeq1</span>. <span class="id" title="tactic">apply</span> <span class="id" title="var">IHT1_2</span> <span class="id" title="keyword">in</span> <span class="id" title="var">Hbeq2</span>. <span class="id" title="tactic">subst</span>... <span class="id" title="keyword">Qed</span>.<br/>
</div>
<span class="id" title="keyword">End</span> <a class="idref" href="Typechecking.html#STLCTypes"><span class="id" title="module">STLCTypes</span></a>.<br/>
</div>

<div class="doc">
<a id="lab359"></a><h1 class="section">The Typechecker</h1>

<div class="paragraph"> </div>

 The typechecker works by walking over the structure of the given
    term, returning either <span class="inlinecode"><span class="id" title="var">Some</span></span> <span class="inlinecode"><span class="id" title="var">T</span></span> or <span class="inlinecode"><span class="id" title="var">None</span></span>.  Each time we make a
    recursive call to find out the types of the subterms, we need to
    pattern-match on the results to make sure that they are not
    <span class="inlinecode"><span class="id" title="var">None</span></span>.  Also, in the <span class="inlinecode"><span class="id" title="var">app</span></span> case, we use pattern matching to
    extract the left- and right-hand sides of the function's arrow
    type (and fail if the type of the function is not <span class="inlinecode"><span class="id" title="var">T<sub>11</sub></span>→<span class="id" title="var">T<sub>12</sub></span></span>
    for some <span class="inlinecode"><span class="id" title="var">T<sub>11</sub></span></span> and <span class="inlinecode"><span class="id" title="var">T<sub>12</sub></span></span>). 
</div>
<div class="code">

<span class="id" title="keyword">Module</span> <a id="FirstTry" class="idref" href="#FirstTry"><span class="id" title="module">FirstTry</span></a>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">STLCTypes</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Fixpoint</span> <a id="FirstTry.type_check" class="idref" href="#FirstTry.type_check"><span class="id" title="definition">type_check</span></a> (<a id="Gamma:9" class="idref" href="#Gamma:9"><span class="id" title="binder">Gamma</span></a> : <a class="idref" href="Stlc.html#STLC.context"><span class="id" title="definition">context</span></a>) (<a id="t:10" class="idref" href="#t:10"><span class="id" title="binder">t</span></a> : <a class="idref" href="Stlc.html#STLC.tm"><span class="id" title="inductive">tm</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="Stlc.html#STLC.ty"><span class="id" title="inductive">ty</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#t:10"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#STLC.tm_var"><span class="id" title="constructor">tm_var</span></a> <span class="id" title="var">x</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Typechecking.html#Gamma:9"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">x</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><span class="id" title="var">x</span><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><span class="id" title="var">T<sub>2</sub></span><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#type_check:11"><span class="id" title="definition">type_check</span></a> (<span class="id" title="var">x</span> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <span class="id" title="var">T<sub>2</sub></span> <span class="id" title="notation">;</span> <a class="idref" href="Typechecking.html#Gamma:9"><span class="id" title="variable">Gamma</span></a>) <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T<sub>1</sub></span> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><span class="id" title="var">T<sub>2</sub></span><a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a><span class="id" title="var">T<sub>1</sub></span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub></span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#type_check:11"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:9"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">t<sub>1</sub></span>, <a class="idref" href="Typechecking.html#type_check:11"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:9"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">t<sub>2</sub></span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><span class="id" title="var">T<sub>11</sub></span><a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a><span class="id" title="var">T<sub>12</sub></span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a>, <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T<sub>2</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="Typechecking.html#STLCTypes.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>11</sub></span> <span class="id" title="var">T<sub>2</sub></span> <span class="id" title="keyword">then</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T<sub>12</sub></span> <span class="id" title="keyword">else</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span>,<span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'true'"><span class="id" title="notation">true</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'false'"><span class="id" title="notation">false</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <span class="id" title="var">guard</span> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <span class="id" title="var">t</span> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <span class="id" title="var">f</span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#type_check:11"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:9"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">guard</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#type_check:11"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:9"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Typechecking.html#t:10"><span class="id" title="variable">t</span></a>, <a class="idref" href="Typechecking.html#type_check:11"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:9"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">f</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T<sub>1</sub></span>, <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T<sub>2</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="Typechecking.html#STLCTypes.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>2</sub></span> <span class="id" title="keyword">then</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T<sub>1</sub></span> <span class="id" title="keyword">else</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span>,<span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">End</span> <a class="idref" href="Typechecking.html#FirstTry"><span class="id" title="module">FirstTry</span></a>.<br/>
</div>

<div class="doc">
<a id="lab360"></a><h1 class="section">Digression: Improving the Notation</h1>

<div class="paragraph"> </div>

 Before we consider the properties of this algorithm, let's write
    it out again in a cleaner way, using "monadic" notations in the
    style of Haskell to streamline the plumbing of options.  First, we
    define a notation for composing two potentially failing (i.e.,
    option-returning) computations: 
</div>
<div class="code">

<span class="id" title="keyword">Notation</span> <a id="f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>" class="idref" href="#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&quot;</span></a> x &lt;- e<sub>1</sub> ;; e<sub>2</sub>" := (<span class="id" title="keyword">match</span> <span class="id" title="var">e<sub>1</sub></span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">x</span> ⇒ <span class="id" title="var">e<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" title="tactic">right</span> <span class="id" title="keyword">associativity</span>, <span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/>
</div>

<div class="doc">
Second, we define <span class="inlinecode"><span class="id" title="keyword">return</span></span> and <span class="inlinecode"><span class="id" title="tactic">fail</span></span> as synonyms for <span class="inlinecode"><span class="id" title="var">Some</span></span> and
    <span class="inlinecode"><span class="id" title="var">None</span></span>: 
</div>
<div class="code">

<span class="id" title="keyword">Notation</span> <a id=":::'return'_x" class="idref" href="#:::'return'_x"><span class="id" title="notation">&quot;</span></a> 'return' e "<br/>
&nbsp;&nbsp;:= (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">e</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 60).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Notation</span> <a id=":::'fail'" class="idref" href="#:::'fail'"><span class="id" title="notation">&quot;</span></a> 'fail' "<br/>
&nbsp;&nbsp;:= <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Module</span> <a id="STLCChecker" class="idref" href="#STLCChecker"><span class="id" title="module">STLCChecker</span></a>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">STLCTypes</span>.<br/>
</div>

<div class="doc">
Now we can write the same type-checking function in a more
    imperative-looking style using these notations. 
</div>
<div class="code">

<span class="id" title="keyword">Fixpoint</span> <a id="STLCChecker.type_check" class="idref" href="#STLCChecker.type_check"><span class="id" title="definition">type_check</span></a> (<a id="Gamma:13" class="idref" href="#Gamma:13"><span class="id" title="binder">Gamma</span></a> : <a class="idref" href="Stlc.html#STLC.context"><span class="id" title="definition">context</span></a>) (<a id="t:14" class="idref" href="#t:14"><span class="id" title="binder">t</span></a> : <a class="idref" href="Stlc.html#STLC.tm"><span class="id" title="inductive">tm</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="Stlc.html#STLC.ty"><span class="id" title="inductive">ty</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#t:14"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#STLC.tm_var"><span class="id" title="constructor">tm_var</span></a> <span class="id" title="var">x</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#Gamma:13"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">x</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T</span> ⇒ <a class="idref" href="Typechecking.html#:::'return'_x"><span class="id" title="notation">return</span></a> <span class="id" title="var">T</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>   ⇒ <a class="idref" href="Typechecking.html#:::'fail'"><span class="id" title="notation">fail</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">\</span></a><span class="id" title="var">x</span><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">:</span></a><span class="id" title="var">T<sub>2</sub></span><a class="idref" href="Stlc.html#28c1f0fbf2e9b1fd5a138d34ed0aa145"><span class="id" title="notation">,</span></a> <span class="id" title="var">t<sub>1</sub></span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="T<sub>1</sub>:17" class="idref" href="#T<sub>1</sub>:17"><span class="id" title="binder">T<sub>1</sub></span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:15"><span class="id" title="definition">type_check</span></a> (<span class="id" title="var">x</span> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <span class="id" title="var">T<sub>2</sub></span> <span class="id" title="notation">;</span> <a class="idref" href="Typechecking.html#Gamma:13"><span class="id" title="variable">Gamma</span></a>) <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Typechecking.html#:::'return'_x"><span class="id" title="notation">return</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><span class="id" title="var">T<sub>2</sub></span><a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a><a class="idref" href="Typechecking.html#T<sub>1</sub>:17"><span class="id" title="variable">T<sub>1</sub></span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub></span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="T<sub>1</sub>:18" class="idref" href="#T<sub>1</sub>:18"><span class="id" title="binder">T<sub>1</sub></span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:15"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:13"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="T<sub>2</sub>:19" class="idref" href="#T<sub>2</sub>:19"><span class="id" title="binder">T<sub>2</sub></span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:15"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:13"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">t<sub>2</sub></span> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#T<sub>1</sub>:18"><span class="id" title="variable">T<sub>1</sub></span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><span class="id" title="var">T<sub>11</sub></span><a class="idref" href="Stlc.html#STLC.:stlc::x_'-&gt;'_x"><span class="id" title="notation">→</span></a><span class="id" title="var">T<sub>12</sub></span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="Typechecking.html#STLCTypes.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>11</sub></span> <a class="idref" href="Typechecking.html#T<sub>2</sub>:19"><span class="id" title="variable">T<sub>2</sub></span></a> <span class="id" title="keyword">then</span> <a class="idref" href="Typechecking.html#:::'return'_x"><span class="id" title="notation">return</span></a> <span class="id" title="var">T<sub>12</sub></span> <span class="id" title="keyword">else</span> <a class="idref" href="Typechecking.html#:::'fail'"><span class="id" title="notation">fail</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span> ⇒ <a class="idref" href="Typechecking.html#:::'fail'"><span class="id" title="notation">fail</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'true'"><span class="id" title="notation">true</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Typechecking.html#:::'return'_x"><span class="id" title="notation">return</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'false'"><span class="id" title="notation">false</span></a><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Typechecking.html#:::'return'_x"><span class="id" title="notation">return</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a><a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">if</span></a> <span class="id" title="var">guard</span> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="Stlc.html#STLC.:stlc::'if'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <span class="id" title="var">t<sub>2</sub></span><a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="Tguard:21" class="idref" href="#Tguard:21"><span class="id" title="binder">Tguard</span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:15"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:13"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">guard</span> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="T<sub>1</sub>:22" class="idref" href="#T<sub>1</sub>:22"><span class="id" title="binder">T<sub>1</sub></span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:15"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:13"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="T<sub>2</sub>:23" class="idref" href="#T<sub>2</sub>:23"><span class="id" title="binder">T<sub>2</sub></span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:15"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:13"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">t<sub>2</sub></span> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#Tguard:21"><span class="id" title="variable">Tguard</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="Stlc.html#STLC.:stlc::'Bool'"><span class="id" title="notation">Bool</span></a> <a class="idref" href="Stlc.html#eaa77420ac6a1aef5b440889c7543807"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="Typechecking.html#STLCTypes.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> <a class="idref" href="Typechecking.html#T<sub>1</sub>:22"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="Typechecking.html#T<sub>2</sub>:23"><span class="id" title="variable">T<sub>2</sub></span></a> <span class="id" title="keyword">then</span> <a class="idref" href="Typechecking.html#:::'return'_x"><span class="id" title="notation">return</span></a> <a class="idref" href="Typechecking.html#T<sub>1</sub>:22"><span class="id" title="variable">T<sub>1</sub></span></a> <span class="id" title="keyword">else</span> <a class="idref" href="Typechecking.html#:::'fail'"><span class="id" title="notation">fail</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span> ⇒ <a class="idref" href="Typechecking.html#:::'fail'"><span class="id" title="notation">fail</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
<a id="lab361"></a><h1 class="section">Properties</h1>

<div class="paragraph"> </div>

 To verify that the typechecking algorithm is correct, we show that
    it is <i>sound</i> and <i>complete</i> for the original <span class="inlinecode"><span class="id" title="var">has_type</span></span>
    relation -- that is, <span class="inlinecode"><span class="id" title="var">type_check</span></span> and <span class="inlinecode"><span class="id" title="var">has_type</span></span> define the same
    partial function. 
</div>
<div class="code">

<span class="id" title="keyword">Theorem</span> <a id="STLCChecker.type_checking_sound" class="idref" href="#STLCChecker.type_checking_sound"><span class="id" title="lemma">type_checking_sound</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:25" class="idref" href="#Gamma:25"><span class="id" title="binder">Gamma</span></a> <a id="t:26" class="idref" href="#t:26"><span class="id" title="binder">t</span></a> <a id="T:27" class="idref" href="#T:27"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Typechecking.html#STLCChecker.type_check"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:25"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Typechecking.html#t:26"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Typechecking.html#T:27"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Stlc.html#STLC.has_type"><span class="id" title="inductive">has_type</span></a> <a class="idref" href="Typechecking.html#Gamma:25"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Typechecking.html#t:26"><span class="id" title="variable">t</span></a> <a class="idref" href="Typechecking.html#T:27"><span class="id" title="variable">T</span></a>.<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t</span>. <span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">t</span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">T</span> <span class="id" title="var">Htc</span>; <span class="id" title="tactic">inversion</span> <span class="id" title="var">Htc</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;var&nbsp;*)</span> <span class="id" title="tactic">rename</span> <span class="id" title="var">s</span> <span class="id" title="var">into</span> <span class="id" title="var">x</span>. <span class="id" title="tactic">destruct</span> (<span class="id" title="var">Gamma</span> <span class="id" title="var">x</span>) <span class="id" title="var">eqn</span>:<span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rename</span> <span class="id" title="var">t</span> <span class="id" title="var">into</span> <span class="id" title="var">T'</span>. <span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>0</sub></span>. <span class="id" title="tactic">subst</span>. <span class="id" title="tactic">eauto</span>. <span class="id" title="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;app&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">remember</span> (<a class="idref" href="Typechecking.html#STLCChecker.type_check"><span class="id" title="definition">type_check</span></a> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>1</sub></span>) <span class="id" title="keyword">as</span> <span class="id" title="var">TO<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">TO<sub>1</sub></span> <span class="id" title="keyword">as</span> [<span class="id" title="var">T<sub>1</sub></span>|]; <span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">T<sub>1</sub></span> <span class="id" title="keyword">as</span> [|<span class="id" title="var">T<sub>11</sub></span> <span class="id" title="var">T<sub>12</sub></span>]; <span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">remember</span> (<a class="idref" href="Typechecking.html#STLCChecker.type_check"><span class="id" title="definition">type_check</span></a> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>2</sub></span>) <span class="id" title="keyword">as</span> <span class="id" title="var">TO<sub>2</sub></span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">TO<sub>2</sub></span> <span class="id" title="keyword">as</span> [<span class="id" title="var">T<sub>2</sub></span>|]; <span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> (<a class="idref" href="Typechecking.html#STLCTypes.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>11</sub></span> <span class="id" title="var">T<sub>2</sub></span>) <span class="id" title="var">eqn</span>: <span class="id" title="var">Heqb</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Typechecking.html#STLCTypes.eqb_ty__eq"><span class="id" title="lemma">eqb_ty__eq</span></a> <span class="id" title="keyword">in</span> <span class="id" title="var">Heqb</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>0</sub></span>; <span class="id" title="tactic">subst</span>...<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>0</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;abs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rename</span> <span class="id" title="var">s</span> <span class="id" title="var">into</span> <span class="id" title="var">x</span>, <span class="id" title="var">t</span> <span class="id" title="var">into</span> <span class="id" title="var">T<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">remember</span> (<span class="id" title="var">x</span> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <span class="id" title="var">T<sub>1</sub></span> <span class="id" title="notation">;</span> <span class="id" title="var">Gamma</span>) <span class="id" title="keyword">as</span> <span class="id" title="var">G'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">remember</span> (<a class="idref" href="Typechecking.html#STLCChecker.type_check"><span class="id" title="definition">type_check</span></a> <span class="id" title="var">G'</span> <span class="id" title="var">t<sub>0</sub></span>) <span class="id" title="keyword">as</span> <span class="id" title="var">TO<sub>2</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">TO<sub>2</sub></span>; <span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>0</sub></span>; <span class="id" title="tactic">subst</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;tru&nbsp;*)</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;fls&nbsp;*)</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;test&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">remember</span> (<a class="idref" href="Typechecking.html#STLCChecker.type_check"><span class="id" title="definition">type_check</span></a> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>1</sub></span>) <span class="id" title="keyword">as</span> <span class="id" title="var">TOc</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">remember</span> (<a class="idref" href="Typechecking.html#STLCChecker.type_check"><span class="id" title="definition">type_check</span></a> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>2</sub></span>) <span class="id" title="keyword">as</span> <span class="id" title="var">TO<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">remember</span> (<a class="idref" href="Typechecking.html#STLCChecker.type_check"><span class="id" title="definition">type_check</span></a> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>3</sub></span>) <span class="id" title="keyword">as</span> <span class="id" title="var">TO<sub>2</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">TOc</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">Tc</span>|]; <span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">Tc</span>; <span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">TO<sub>1</sub></span> <span class="id" title="keyword">as</span> [<span class="id" title="var">T<sub>1</sub></span>|]; <span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">TO<sub>2</sub></span> <span class="id" title="keyword">as</span> [<span class="id" title="var">T<sub>2</sub></span>|]; <span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> (<a class="idref" href="Typechecking.html#STLCTypes.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>2</sub></span>) <span class="id" title="var">eqn</span>:<span class="id" title="var">Heqb</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="Typechecking.html#STLCTypes.eqb_ty__eq"><span class="id" title="lemma">eqb_ty__eq</span></a> <span class="id" title="keyword">in</span> <span class="id" title="var">Heqb</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>0</sub></span>. <span class="id" title="tactic">subst</span>. <span class="id" title="tactic">subst</span>...<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" title="keyword">Theorem</span> <a id="STLCChecker.type_checking_complete" class="idref" href="#STLCChecker.type_checking_complete"><span class="id" title="lemma">type_checking_complete</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:28" class="idref" href="#Gamma:28"><span class="id" title="binder">Gamma</span></a> <a id="t:29" class="idref" href="#t:29"><span class="id" title="binder">t</span></a> <a id="T:30" class="idref" href="#T:30"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Stlc.html#STLC.has_type"><span class="id" title="inductive">has_type</span></a> <a class="idref" href="Typechecking.html#Gamma:28"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Typechecking.html#t:29"><span class="id" title="variable">t</span></a> <a class="idref" href="Typechecking.html#T:30"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Typechecking.html#STLCChecker.type_check"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:28"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Typechecking.html#t:29"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Typechecking.html#T:30"><span class="id" title="variable">T</span></a>.<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">auto</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t</span> <span class="id" title="var">T</span> <span class="id" title="var">Hty</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">Hty</span>; <span class="id" title="tactic">simpl</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Var&nbsp;*)</span> <span class="id" title="tactic">destruct</span> (<span class="id" title="var">Gamma</span> <span class="id" title="var">x<sub>0</sub></span>) <span class="id" title="var">eqn</span>:<span class="id" title="var">H<sub>0</sub></span>; <span class="id" title="tactic">assumption</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_Abs&nbsp;*)</span> <span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHHty</span>...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_App&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHHty1</span>. <span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHHty2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> (<a class="idref" href="Typechecking.html#STLCTypes.eqb_ty_refl"><span class="id" title="lemma">eqb_ty_refl</span></a> <span class="id" title="var">T<sub>2</sub></span>)...<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_True&nbsp;*)</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_False&nbsp;*)</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;T_If&nbsp;*)</span> <span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHHty1</span>. <span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHHty2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHHty3</span>. <span class="id" title="tactic">rewrite</span> (<a class="idref" href="Typechecking.html#STLCTypes.eqb_ty_refl"><span class="id" title="lemma">eqb_ty_refl</span></a> <span class="id" title="var">T<sub>1</sub></span>)...<br/>
<span class="id" title="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Typechecking.html#STLCChecker"><span class="id" title="module">STLCChecker</span></a>.<br/>
</div>

<div class="doc">
<a id="lab362"></a><h1 class="section">Exercises</h1>

<div class="paragraph"> </div>

<a id="lab363"></a><h4 class="section">Exercise: 5 stars, standard (typechecker_extensions)</h4>
 In this exercise we'll extend the typechecker to deal with the
    extended features discussed in chapter <a href="MoreStlc.html"><span class="inlineref">MoreStlc</span></a>.  Your job
    is to fill in the omitted cases in the following. 
</div>
<div class="code">

<span class="id" title="keyword">Module</span> <a id="TypecheckerExtensions" class="idref" href="#TypecheckerExtensions"><span class="id" title="module">TypecheckerExtensions</span></a>.<br/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="TypecheckerExtensions.manual_grade_for_type_checking_sound" class="idref" href="#TypecheckerExtensions.manual_grade_for_type_checking_sound"><span class="id" title="definition">manual_grade_for_type_checking_sound</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<span class="comment">(*&nbsp;Do&nbsp;not&nbsp;modify&nbsp;the&nbsp;following&nbsp;line:&nbsp;*)</span><br/>
<span class="id" title="keyword">Definition</span> <a id="TypecheckerExtensions.manual_grade_for_type_checking_complete" class="idref" href="#TypecheckerExtensions.manual_grade_for_type_checking_complete"><span class="id" title="definition">manual_grade_for_type_checking_complete</span></a> : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> (<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#nat"><span class="id" title="inductive">nat</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#11c698c8685bb8ab1cf725545c085ac<sub>4</sub>"><span class="id" title="notation">×</span></a><a class="idref" href="http://coq.inria.fr/library//Coq.Strings.String.html#string"><span class="id" title="inductive">string</span></a>) := <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">MoreStlc</span>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">STLCExtended</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Fixpoint</span> <a id="TypecheckerExtensions.eqb_ty" class="idref" href="#TypecheckerExtensions.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> (<a id="T<sub>1</sub>:31" class="idref" href="#T<sub>1</sub>:31"><span class="id" title="binder">T<sub>1</sub></span></a> <a id="T<sub>2</sub>:32" class="idref" href="#T<sub>2</sub>:32"><span class="id" title="binder">T<sub>2</sub></span></a> : <a class="idref" href="MoreStlc.html#STLCExtended.ty"><span class="id" title="inductive">ty</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#bool"><span class="id" title="inductive">bool</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#T<sub>1</sub>:31"><span class="id" title="variable">T<sub>1</sub></span></a>,<a class="idref" href="Typechecking.html#T<sub>2</sub>:32"><span class="id" title="variable">T<sub>2</sub></span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'Nat'"><span class="id" title="notation">Nat</span></a><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a>, <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'Nat'"><span class="id" title="notation">Nat</span></a><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'Unit'"><span class="id" title="notation">Unit</span></a><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a>, <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'Unit'"><span class="id" title="notation">Unit</span></a><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><span class="id" title="var">T<sub>11</sub></span> <a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="var">T<sub>12</sub></span><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a>, <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><span class="id" title="var">T<sub>21</sub></span> <a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="var">T<sub>22</sub></span><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#andb"><span class="id" title="definition">andb</span></a> (<a class="idref" href="Typechecking.html#eqb_ty:33"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>11</sub></span> <span class="id" title="var">T<sub>21</sub></span>) (<a class="idref" href="Typechecking.html#eqb_ty:33"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>12</sub></span> <span class="id" title="var">T<sub>22</sub></span>)<br/>
&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><span class="id" title="var">T<sub>11</sub></span> <a class="idref" href="MoreStlc.html#07385bcfe759c5c52b9f596e53f2c0f<sub>5</sub>"><span class="id" title="notation">×</span></a> <span class="id" title="var">T<sub>12</sub></span><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a>, <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><span class="id" title="var">T<sub>21</sub></span> <a class="idref" href="MoreStlc.html#07385bcfe759c5c52b9f596e53f2c0f<sub>5</sub>"><span class="id" title="notation">×</span></a> <span class="id" title="var">T<sub>22</sub></span><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#andb"><span class="id" title="definition">andb</span></a> (<a class="idref" href="Typechecking.html#eqb_ty:33"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>11</sub></span> <span class="id" title="var">T<sub>21</sub></span>) (<a class="idref" href="Typechecking.html#eqb_ty:33"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>12</sub></span> <span class="id" title="var">T<sub>22</sub></span>)<br/>
&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><span class="id" title="var">T<sub>11</sub></span> <a class="idref" href="MoreStlc.html#8d02d86020db13ec74895c11a9bd9e<sub>25</sub>"><span class="id" title="notation">+</span></a> <span class="id" title="var">T<sub>12</sub></span><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a>, <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><span class="id" title="var">T<sub>21</sub></span> <a class="idref" href="MoreStlc.html#8d02d86020db13ec74895c11a9bd9e<sub>25</sub>"><span class="id" title="notation">+</span></a> <span class="id" title="var">T<sub>22</sub></span><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#andb"><span class="id" title="definition">andb</span></a> (<a class="idref" href="Typechecking.html#eqb_ty:33"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>11</sub></span> <span class="id" title="var">T<sub>21</sub></span>) (<a class="idref" href="Typechecking.html#eqb_ty:33"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>12</sub></span> <span class="id" title="var">T<sub>22</sub></span>)<br/>
&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'List'_x"><span class="id" title="notation">List</span></a> <span class="id" title="var">T<sub>11</sub></span><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a>, <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'List'_x"><span class="id" title="notation">List</span></a> <span class="id" title="var">T<sub>21</sub></span><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Typechecking.html#eqb_ty:33"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>11</sub></span> <span class="id" title="var">T<sub>21</sub></span><br/>
&nbsp;&nbsp;| <span class="id" title="var">_</span>,<span class="id" title="var">_</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#false"><span class="id" title="constructor">false</span></a><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Lemma</span> <a id="TypecheckerExtensions.eqb_ty_refl" class="idref" href="#TypecheckerExtensions.eqb_ty_refl"><span class="id" title="lemma">eqb_ty_refl</span></a> : <span class="id" title="keyword">∀</span> <a id="T:36" class="idref" href="#T:36"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Typechecking.html#TypecheckerExtensions.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> <a class="idref" href="Typechecking.html#T:36"><span class="id" title="variable">T</span></a> <a class="idref" href="Typechecking.html#T:36"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">T</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">T</span>; <span class="id" title="tactic">simpl</span>; <span class="id" title="tactic">auto</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHT1</span>; <span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHT2</span>; <span class="id" title="tactic">reflexivity</span>. <span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Lemma</span> <a id="TypecheckerExtensions.eqb_ty__eq" class="idref" href="#TypecheckerExtensions.eqb_ty__eq"><span class="id" title="lemma">eqb_ty__eq</span></a> : <span class="id" title="keyword">∀</span> <a id="T<sub>1</sub>:37" class="idref" href="#T<sub>1</sub>:37"><span class="id" title="binder">T<sub>1</sub></span></a> <a id="T<sub>2</sub>:38" class="idref" href="#T<sub>2</sub>:38"><span class="id" title="binder">T<sub>2</sub></span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Typechecking.html#TypecheckerExtensions.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> <a class="idref" href="Typechecking.html#T<sub>1</sub>:37"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="Typechecking.html#T<sub>2</sub>:38"><span class="id" title="variable">T<sub>2</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#true"><span class="id" title="constructor">true</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Typechecking.html#T<sub>1</sub>:37"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="Typechecking.html#T<sub>2</sub>:38"><span class="id" title="variable">T<sub>2</sub></span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">T<sub>1</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">T<sub>1</sub></span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">T<sub>2</sub></span> <span class="id" title="var">Hbeq</span>; <span class="id" title="tactic">destruct</span> <span class="id" title="var">T<sub>2</sub></span>; <span class="id" title="tactic">inversion</span> <span class="id" title="var">Hbeq</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">try</span> <span class="id" title="tactic">reflexivity</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">try</span> (<span class="id" title="tactic">rewrite</span> <a class="idref" href="http://coq.inria.fr/library//Coq.Bool.Bool.html#andb_true_iff"><span class="id" title="lemma">andb_true_iff</span></a> <span class="id" title="keyword">in</span> <span class="id" title="var">H<sub>0</sub></span>; <span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>0</sub></span> <span class="id" title="keyword">as</span> [<span class="id" title="var">Hbeq1</span> <span class="id" title="var">Hbeq2</span>];<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <span class="id" title="var">IHT1_1</span> <span class="id" title="keyword">in</span> <span class="id" title="var">Hbeq1</span>; <span class="id" title="tactic">apply</span> <span class="id" title="var">IHT1_2</span> <span class="id" title="keyword">in</span> <span class="id" title="var">Hbeq2</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">auto</span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">try</span> (<span class="id" title="tactic">apply</span> <span class="id" title="var">IHT1</span> <span class="id" title="keyword">in</span> <span class="id" title="var">Hbeq</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">auto</span>).<br/>
&nbsp;<span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Fixpoint</span> <a id="TypecheckerExtensions.type_check" class="idref" href="#TypecheckerExtensions.type_check"><span class="id" title="definition">type_check</span></a> (<a id="Gamma:39" class="idref" href="#Gamma:39"><span class="id" title="binder">Gamma</span></a> : <a class="idref" href="MoreStlc.html#STLCExtended.context"><span class="id" title="definition">context</span></a>) (<a id="t:40" class="idref" href="#t:40"><span class="id" title="binder">t</span></a> : <a class="idref" href="MoreStlc.html#STLCExtended.tm"><span class="id" title="inductive">tm</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="MoreStlc.html#STLCExtended.ty"><span class="id" title="inductive">ty</span></a> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#t:40"><span class="id" title="variable">t</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#STLCExtended.tm_var"><span class="id" title="constructor">tm_var</span></a> <span class="id" title="var">x</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#Gamma:39"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">x</span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T</span> ⇒ <a class="idref" href="Typechecking.html#:::'return'_x"><span class="id" title="notation">return</span></a> <span class="id" title="var">T</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>   ⇒ <a class="idref" href="Typechecking.html#:::'fail'"><span class="id" title="notation">fail</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#9593265f23640347d8baf3ded78adc0e"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="MoreStlc.html#1ad52bf8598c9e0c39505628d95be60b"><span class="id" title="notation">\</span></a> <span class="id" title="var">x<sub>1</sub></span> <a class="idref" href="MoreStlc.html#1ad52bf8598c9e0c39505628d95be60b"><span class="id" title="notation">:</span></a> <span class="id" title="var">T<sub>1</sub></span><a class="idref" href="MoreStlc.html#1ad52bf8598c9e0c39505628d95be60b"><span class="id" title="notation">,</span></a> <span class="id" title="var">t<sub>2</sub></span> <a class="idref" href="MoreStlc.html#9593265f23640347d8baf3ded78adc0e"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="T<sub>2</sub>:43" class="idref" href="#T<sub>2</sub>:43"><span class="id" title="binder">T<sub>2</sub></span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:41"><span class="id" title="definition">type_check</span></a> (<span class="id" title="var">x<sub>1</sub></span> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <span class="id" title="var">T<sub>1</sub></span> <span class="id" title="notation">;</span> <a class="idref" href="Typechecking.html#Gamma:39"><span class="id" title="variable">Gamma</span></a>) <span class="id" title="var">t<sub>2</sub></span> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Typechecking.html#:::'return'_x"><span class="id" title="notation">return</span></a> <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><span class="id" title="var">T<sub>1</sub></span> <a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <a class="idref" href="Typechecking.html#T<sub>2</sub>:43"><span class="id" title="variable">T<sub>2</sub></span></a><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#9593265f23640347d8baf3ded78adc0e"><span class="id" title="notation">&lt;{</span></a> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">t<sub>2</sub></span> <a class="idref" href="MoreStlc.html#9593265f23640347d8baf3ded78adc0e"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="T<sub>1</sub>:44" class="idref" href="#T<sub>1</sub>:44"><span class="id" title="binder">T<sub>1</sub></span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:41"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:39"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="T<sub>2</sub>:45" class="idref" href="#T<sub>2</sub>:45"><span class="id" title="binder">T<sub>2</sub></span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:41"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:39"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">t<sub>2</sub></span> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#T<sub>1</sub>:44"><span class="id" title="variable">T<sub>1</sub></span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><span class="id" title="var">T<sub>11</sub></span> <a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::x_'-&gt;'_x"><span class="id" title="notation">→</span></a> <span class="id" title="var">T<sub>12</sub></span><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="Typechecking.html#TypecheckerExtensions.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>11</sub></span> <a class="idref" href="Typechecking.html#T<sub>2</sub>:45"><span class="id" title="variable">T<sub>2</sub></span></a> <span class="id" title="keyword">then</span> <a class="idref" href="Typechecking.html#:::'return'_x"><span class="id" title="notation">return</span></a> <span class="id" title="var">T<sub>12</sub></span> <span class="id" title="keyword">else</span> <a class="idref" href="Typechecking.html#:::'fail'"><span class="id" title="notation">fail</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span> ⇒ <a class="idref" href="Typechecking.html#:::'fail'"><span class="id" title="notation">fail</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#STLCExtended.tm_const"><span class="id" title="constructor">tm_const</span></a> <span class="id" title="var">_</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Typechecking.html#:::'return'_x"><span class="id" title="notation">return</span></a> <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'Nat'"><span class="id" title="notation">Nat</span></a><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a><br/>
&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#9593265f23640347d8baf3ded78adc0e"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="MoreStlc.html#STLCExtended.:stlc::'succ'_x"><span class="id" title="notation">succ</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="MoreStlc.html#9593265f23640347d8baf3ded78adc0e"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="T<sub>1</sub>:47" class="idref" href="#T<sub>1</sub>:47"><span class="id" title="binder">T<sub>1</sub></span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:41"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:39"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#T<sub>1</sub>:47"><span class="id" title="variable">T<sub>1</sub></span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'Nat'"><span class="id" title="notation">Nat</span></a><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a> ⇒ <a class="idref" href="Typechecking.html#:::'return'_x"><span class="id" title="notation">return</span></a> <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'Nat'"><span class="id" title="notation">Nat</span></a><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span> ⇒ <a class="idref" href="Typechecking.html#:::'fail'"><span class="id" title="notation">fail</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#9593265f23640347d8baf3ded78adc0e"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="MoreStlc.html#STLCExtended.:stlc::'pred'_x"><span class="id" title="notation">pred</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="MoreStlc.html#9593265f23640347d8baf3ded78adc0e"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="T<sub>1</sub>:49" class="idref" href="#T<sub>1</sub>:49"><span class="id" title="binder">T<sub>1</sub></span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:41"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:39"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#T<sub>1</sub>:49"><span class="id" title="variable">T<sub>1</sub></span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'Nat'"><span class="id" title="notation">Nat</span></a><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a> ⇒ <a class="idref" href="Typechecking.html#:::'return'_x"><span class="id" title="notation">return</span></a> <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'Nat'"><span class="id" title="notation">Nat</span></a><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span> ⇒ <a class="idref" href="Typechecking.html#:::'fail'"><span class="id" title="notation">fail</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#9593265f23640347d8baf3ded78adc0e"><span class="id" title="notation">&lt;{</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="MoreStlc.html#43eb4b39e17c20cb1da938909e269aa<sub>6</sub>"><span class="id" title="notation">×</span></a> <span class="id" title="var">t<sub>2</sub></span> <a class="idref" href="MoreStlc.html#9593265f23640347d8baf3ded78adc0e"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="T<sub>1</sub>:51" class="idref" href="#T<sub>1</sub>:51"><span class="id" title="binder">T<sub>1</sub></span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:41"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:39"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="T<sub>2</sub>:52" class="idref" href="#T<sub>2</sub>:52"><span class="id" title="binder">T<sub>2</sub></span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:41"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:39"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">t<sub>2</sub></span> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#T<sub>1</sub>:51"><span class="id" title="variable">T<sub>1</sub></span></a>, <a class="idref" href="Typechecking.html#T<sub>2</sub>:52"><span class="id" title="variable">T<sub>2</sub></span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'Nat'"><span class="id" title="notation">Nat</span></a><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a>, <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'Nat'"><span class="id" title="notation">Nat</span></a><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a> ⇒ <a class="idref" href="Typechecking.html#:::'return'_x"><span class="id" title="notation">return</span></a> <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'Nat'"><span class="id" title="notation">Nat</span></a><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span>,<span class="id" title="var">_</span>        ⇒ <a class="idref" href="Typechecking.html#:::'fail'"><span class="id" title="notation">fail</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#9593265f23640347d8baf3ded78adc0e"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="MoreStlc.html#STLCExtended.:stlc::'if<sub>0</sub>'_x_'then'_x_'else'_x"><span class="id" title="notation">if<sub>0</sub></span></a> <span class="id" title="var">guard</span> <a class="idref" href="MoreStlc.html#STLCExtended.:stlc::'if<sub>0</sub>'_x_'then'_x_'else'_x"><span class="id" title="notation">then</span></a> <span class="id" title="var">t</span> <a class="idref" href="MoreStlc.html#STLCExtended.:stlc::'if<sub>0</sub>'_x_'then'_x_'else'_x"><span class="id" title="notation">else</span></a> <span class="id" title="var">f</span> <a class="idref" href="MoreStlc.html#9593265f23640347d8baf3ded78adc0e"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="Tguard:55" class="idref" href="#Tguard:55"><span class="id" title="binder">Tguard</span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:41"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:39"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">guard</span> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="T<sub>1</sub>:56" class="idref" href="#T<sub>1</sub>:56"><span class="id" title="binder">T<sub>1</sub></span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:41"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:39"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Typechecking.html#t:40"><span class="id" title="variable">t</span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a id="T<sub>2</sub>:57" class="idref" href="#T<sub>2</sub>:57"><span class="id" title="binder">T<sub>2</sub></span></a> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">&lt;-</span></a> <a class="idref" href="Typechecking.html#type_check:41"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:39"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">f</span> <a class="idref" href="Typechecking.html#f4c072b7f26484005a9e0c3986ed1f<sub>19</sub>"><span class="id" title="notation">;;</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#Tguard:55"><span class="id" title="variable">Tguard</span></a> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'Nat'"><span class="id" title="notation">Nat</span></a><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a> ⇒ <span class="id" title="keyword">if</span> <a class="idref" href="Typechecking.html#TypecheckerExtensions.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> <a class="idref" href="Typechecking.html#T<sub>1</sub>:56"><span class="id" title="variable">T<sub>1</sub></span></a> <a class="idref" href="Typechecking.html#T<sub>2</sub>:57"><span class="id" title="variable">T<sub>2</sub></span></a> <span class="id" title="keyword">then</span> <a class="idref" href="Typechecking.html#:::'return'_x"><span class="id" title="notation">return</span></a> <a class="idref" href="Typechecking.html#T<sub>1</sub>:56"><span class="id" title="variable">T<sub>1</sub></span></a> <span class="id" title="keyword">else</span> <a class="idref" href="Typechecking.html#:::'fail'"><span class="id" title="notation">fail</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span> ⇒ <a class="idref" href="Typechecking.html#:::'fail'"><span class="id" title="notation">fail</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;Complete&nbsp;the&nbsp;following&nbsp;cases.&nbsp;*)</span><br/>
&nbsp;&nbsp;<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;sums&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;lists&nbsp;(the&nbsp;<span class="inlinecode"><span class="id" title="var">tlcase</span></span>&nbsp;is&nbsp;given&nbsp;for&nbsp;free)&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
&nbsp;&nbsp;| <a class="idref" href="MoreStlc.html#9593265f23640347d8baf3ded78adc0e"><span class="id" title="notation">&lt;{</span></a> <a class="idref" href="MoreStlc.html#de876c64e601b25611daf48d0a4b5481"><span class="id" title="notation">case</span></a> <span class="id" title="var">t<sub>0</sub></span> <a class="idref" href="MoreStlc.html#de876c64e601b25611daf48d0a4b5481"><span class="id" title="notation">of</span></a> <a class="idref" href="MoreStlc.html#de876c64e601b25611daf48d0a4b5481"><span class="id" title="notation">|</span></a> <a class="idref" href="MoreStlc.html#de876c64e601b25611daf48d0a4b5481"><span class="id" title="notation">nil</span></a> <a class="idref" href="MoreStlc.html#de876c64e601b25611daf48d0a4b5481"><span class="id" title="notation">⇒</span></a> <span class="id" title="var">t<sub>1</sub></span> <a class="idref" href="MoreStlc.html#de876c64e601b25611daf48d0a4b5481"><span class="id" title="notation">|</span></a> <span class="id" title="var">x<sub>21</sub></span> <a class="idref" href="MoreStlc.html#de876c64e601b25611daf48d0a4b5481"><span class="id" title="notation">::</span></a> <span class="id" title="var">x<sub>22</sub></span> <a class="idref" href="MoreStlc.html#de876c64e601b25611daf48d0a4b5481"><span class="id" title="notation">⇒</span></a> <span class="id" title="var">t<sub>2</sub></span> <a class="idref" href="MoreStlc.html#9593265f23640347d8baf3ded78adc0e"><span class="id" title="notation">}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#type_check:41"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:39"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">t<sub>0</sub></span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'List'_x"><span class="id" title="notation">List</span></a> <span class="id" title="var">T</span><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">match</span> <a class="idref" href="Typechecking.html#type_check:41"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:39"><span class="id" title="variable">Gamma</span></a> <span class="id" title="var">t<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Typechecking.html#type_check:41"><span class="id" title="definition">type_check</span></a> (<span class="id" title="var">x<sub>21</sub></span> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <span class="id" title="var">T</span> <span class="id" title="notation">;</span> <span class="id" title="var">x<sub>22</sub></span> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'List'_x"><span class="id" title="notation">List</span></a> <span class="id" title="var">T</span><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a> <span class="id" title="notation">;</span> <a class="idref" href="Typechecking.html#Gamma:39"><span class="id" title="variable">Gamma</span></a>) <span class="id" title="var">t<sub>2</sub></span> <span class="id" title="keyword">with</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T<sub>1</sub>'</span>, <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <span class="id" title="var">T<sub>2</sub>'</span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">if</span> <a class="idref" href="Typechecking.html#TypecheckerExtensions.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">T<sub>1</sub>'</span> <span class="id" title="var">T<sub>2</sub>'</span> <span class="id" title="keyword">then</span> <a class="idref" href="Typechecking.html#:::'return'_x"><span class="id" title="notation">return</span></a> <span class="id" title="var">T<sub>1</sub>'</span> <span class="id" title="keyword">else</span> <a class="idref" href="Typechecking.html#:::'fail'"><span class="id" title="notation">fail</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span>,<span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">end</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;unit&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;pairs&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;let&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;fix&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
&nbsp;&nbsp;| <span class="id" title="var">_</span> ⇒ <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#None"><span class="id" title="constructor">None</span></a>  <span class="comment">(*&nbsp;...&nbsp;and&nbsp;delete&nbsp;this&nbsp;line&nbsp;when&nbsp;you&nbsp;complete&nbsp;the&nbsp;exercise.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" title="keyword">end</span>.<br/>
</div>

<div class="doc">
Just for fun, we'll do the soundness proof with just a bit more
    automation than above, using these "mega-tactics": 
</div>
<div class="code">

<span class="id" title="keyword">Ltac</span> <span class="id" title="var">invert_typecheck</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t</span> <span class="id" title="var">T</span> :=<br/>
&nbsp;&nbsp;<span class="id" title="var">remember</span> (<a class="idref" href="Typechecking.html#TypecheckerExtensions.type_check"><span class="id" title="definition">type_check</span></a> <span class="id" title="var">Gamma</span> <span class="id" title="var">t</span>) <span class="id" title="keyword">as</span> <span class="id" title="var">TO</span>;<br/>
&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">TO</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">T</span>|];<br/>
&nbsp;&nbsp;<span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>; <span class="id" title="tactic">try</span> (<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>0</sub></span>; <span class="id" title="tactic">eauto</span>); <span class="id" title="tactic">try</span> (<span class="id" title="tactic">subst</span>; <span class="id" title="tactic">eauto</span>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">analyze</span> <span class="id" title="var">T</span> <span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>2</sub></span> :=<br/>
&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">T</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>2</sub></span>| |<span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>2</sub></span>|<span class="id" title="var">T<sub>1</sub></span>| |<span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>2</sub></span>]; <span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">fully_invert_typecheck</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t</span> <span class="id" title="var">T</span> <span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>2</sub></span> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">let</span> <span class="id" title="var">TX</span> := <span class="id" title="tactic">fresh</span> <span class="id" title="var">T</span> <span class="id" title="keyword">in</span><br/>
&nbsp;&nbsp;<span class="id" title="var">remember</span> (<a class="idref" href="Typechecking.html#TypecheckerExtensions.type_check"><span class="id" title="definition">type_check</span></a> <span class="id" title="var">Gamma</span> <span class="id" title="var">t</span>) <span class="id" title="keyword">as</span> <span class="id" title="var">TO</span>;<br/>
&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">TO</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">TX</span>|]; <span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>;<br/>
&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">TX</span> <span class="id" title="keyword">as</span> [<span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>2</sub></span>| |<span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>2</sub></span>|<span class="id" title="var">T<sub>1</sub></span>| |<span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>2</sub></span>];<br/>
&nbsp;&nbsp;<span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>; <span class="id" title="tactic">try</span> (<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>0</sub></span>; <span class="id" title="tactic">eauto</span>); <span class="id" title="tactic">try</span> (<span class="id" title="tactic">subst</span>; <span class="id" title="tactic">eauto</span>).<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">case_equality</span> <span class="id" title="var">S</span> <span class="id" title="var">T</span> :=<br/>
&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> (<a class="idref" href="Typechecking.html#TypecheckerExtensions.eqb_ty"><span class="id" title="definition">eqb_ty</span></a> <span class="id" title="var">S</span> <span class="id" title="var">T</span>) <span class="id" title="var">eqn</span>: <span class="id" title="var">Heqb</span>;<br/>
&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>0</sub></span>; <span class="id" title="tactic">apply</span> <a class="idref" href="Typechecking.html#TypecheckerExtensions.eqb_ty__eq"><span class="id" title="lemma">eqb_ty__eq</span></a> <span class="id" title="keyword">in</span> <span class="id" title="var">Heqb</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">subst</span>; <span class="id" title="tactic">eauto</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="TypecheckerExtensions.type_checking_sound" class="idref" href="#TypecheckerExtensions.type_checking_sound"><span class="id" title="lemma">type_checking_sound</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:59" class="idref" href="#Gamma:59"><span class="id" title="binder">Gamma</span></a> <a id="t:60" class="idref" href="#t:60"><span class="id" title="binder">t</span></a> <a id="T:61" class="idref" href="#T:61"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="Typechecking.html#TypecheckerExtensions.type_check"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:59"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Typechecking.html#t:60"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Typechecking.html#T:61"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="MoreStlc.html#STLCExtended.has_type"><span class="id" title="inductive">has_type</span></a> <a class="idref" href="Typechecking.html#Gamma:59"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Typechecking.html#t:60"><span class="id" title="variable">t</span></a> <a class="idref" href="Typechecking.html#T:61"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span> <span class="id" title="keyword">with</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t</span>. <span class="id" title="tactic">generalize</span> <span class="id" title="tactic">dependent</span> <span class="id" title="var">Gamma</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">t</span>; <span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">T</span> <span class="id" title="var">Htc</span>; <span class="id" title="tactic">inversion</span> <span class="id" title="var">Htc</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;var&nbsp;*)</span> <span class="id" title="tactic">rename</span> <span class="id" title="var">s</span> <span class="id" title="var">into</span> <span class="id" title="var">x</span>. <span class="id" title="tactic">destruct</span> (<span class="id" title="var">Gamma</span> <span class="id" title="var">x</span>) <span class="id" title="var">eqn</span>:<span class="id" title="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rename</span> <span class="id" title="var">t</span> <span class="id" title="var">into</span> <span class="id" title="var">T'</span>. <span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>0</sub></span>. <span class="id" title="tactic">subst</span>. <span class="id" title="tactic">eauto</span>. <span class="id" title="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;app&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">invert_typecheck</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">T<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">invert_typecheck</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>2</sub></span> <span class="id" title="var">T<sub>2</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">analyze</span> <span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>11</sub></span> <span class="id" title="var">T<sub>12</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">case_equality</span> <span class="id" title="var">T<sub>11</sub></span> <span class="id" title="var">T<sub>2</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;abs&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rename</span> <span class="id" title="var">s</span> <span class="id" title="var">into</span> <span class="id" title="var">x</span>, <span class="id" title="var">t</span> <span class="id" title="var">into</span> <span class="id" title="var">T<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">remember</span> (<span class="id" title="var">x</span> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <span class="id" title="var">T<sub>1</sub></span> <span class="id" title="notation">;</span> <span class="id" title="var">Gamma</span>) <span class="id" title="keyword">as</span> <span class="id" title="var">Gamma'</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">invert_typecheck</span> <span class="id" title="var">Gamma'</span> <span class="id" title="var">t<sub>0</sub></span> <span class="id" title="var">T<sub>0</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;const&nbsp;*)</span> <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;scc&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rename</span> <span class="id" title="var">t</span> <span class="id" title="var">into</span> <span class="id" title="var">t<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">fully_invert_typecheck</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>11</sub></span> <span class="id" title="var">T<sub>12</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;prd&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rename</span> <span class="id" title="var">t</span> <span class="id" title="var">into</span> <span class="id" title="var">t<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">fully_invert_typecheck</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>11</sub></span> <span class="id" title="var">T<sub>12</sub></span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;mlt&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">invert_typecheck</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">T<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">invert_typecheck</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>2</sub></span> <span class="id" title="var">T<sub>2</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">analyze</span> <span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>11</sub></span> <span class="id" title="var">T<sub>12</sub></span>; <span class="id" title="var">analyze</span> <span class="id" title="var">T<sub>2</sub></span> <span class="id" title="var">T<sub>21</sub></span> <span class="id" title="var">T<sub>22</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">inversion</span> <span class="id" title="var">H<sub>0</sub></span>. <span class="id" title="tactic">subst</span>. <span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;test0&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">invert_typecheck</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">T<sub>1</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">invert_typecheck</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>2</sub></span> <span class="id" title="var">T<sub>2</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">invert_typecheck</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>3</sub></span> <span class="id" title="var">T<sub>3</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">destruct</span> <span class="id" title="var">T<sub>1</sub></span>; <span class="id" title="tactic">try</span> <span class="id" title="var">solve_by_invert</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">case_equality</span> <span class="id" title="var">T<sub>2</sub></span> <span class="id" title="var">T<sub>3</sub></span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;tlcase&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">rename</span> <span class="id" title="var">s</span> <span class="id" title="var">into</span> <span class="id" title="var">x<sub>31</sub></span>, <span class="id" title="var">s<sub>0</sub></span> <span class="id" title="var">into</span> <span class="id" title="var">x<sub>32</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">fully_invert_typecheck</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>1</sub></span> <span class="id" title="var">T<sub>1</sub></span> <span class="id" title="var">T<sub>11</sub></span> <span class="id" title="var">T<sub>12</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">invert_typecheck</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t<sub>2</sub></span> <span class="id" title="var">T<sub>2</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">remember</span> (<span class="id" title="var">x<sub>31</sub></span> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <span class="id" title="var">T<sub>11</sub></span> <span class="id" title="notation">;</span> <span class="id" title="var">x<sub>32</sub></span> <span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>&#x22A2;</span><span style='font-size:90%;'>&gt;</span></span></span></span></span> <a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation">&lt;<span style='letter-spacing:-.4em;'>{</span>{</span></a><a class="idref" href="MoreStlc.html#STLCExtended.:stlc_ty::'List'_x"><span class="id" title="notation">List</span></a> <span class="id" title="var">T<sub>11</sub></span><a class="idref" href="MoreStlc.html#4790eac4da69227166d84a2e2fa965df"><span class="id" title="notation"><span style='letter-spacing:-.4em;'>}</span>}&gt;</span></a> <span class="id" title="notation">;</span> <span class="id" title="var">Gamma</span>) <span class="id" title="keyword">as</span> <span class="id" title="var">Gamma'2</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">invert_typecheck</span> <span class="id" title="var">Gamma'2</span> <span class="id" title="var">t<sub>3</sub></span> <span class="id" title="var">T<sub>3</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">case_equality</span> <span class="id" title="var">T<sub>2</sub></span> <span class="id" title="var">T<sub>3</sub></span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<span class="id" title="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">Theorem</span> <a id="TypecheckerExtensions.type_checking_complete" class="idref" href="#TypecheckerExtensions.type_checking_complete"><span class="id" title="lemma">type_checking_complete</span></a> : <span class="id" title="keyword">∀</span> <a id="Gamma:62" class="idref" href="#Gamma:62"><span class="id" title="binder">Gamma</span></a> <a id="t:63" class="idref" href="#t:63"><span class="id" title="binder">t</span></a> <a id="T:64" class="idref" href="#T:64"><span class="id" title="binder">T</span></a>,<br/>
&nbsp;&nbsp;<a class="idref" href="MoreStlc.html#STLCExtended.has_type"><span class="id" title="inductive">has_type</span></a> <a class="idref" href="Typechecking.html#Gamma:62"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Typechecking.html#t:63"><span class="id" title="variable">t</span></a> <a class="idref" href="Typechecking.html#T:64"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a><br/>
&nbsp;&nbsp;<a class="idref" href="Typechecking.html#TypecheckerExtensions.type_check"><span class="id" title="definition">type_check</span></a> <a class="idref" href="Typechecking.html#Gamma:62"><span class="id" title="variable">Gamma</span></a> <a class="idref" href="Typechecking.html#t:63"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Typechecking.html#T:64"><span class="id" title="variable">T</span></a>.<br/>
<span class="id" title="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">intros</span> <span class="id" title="var">Gamma</span> <span class="id" title="var">t</span> <span class="id" title="var">T</span> <span class="id" title="var">Hty</span>.<br/>
&nbsp;&nbsp;<span class="id" title="tactic">induction</span> <span class="id" title="var">Hty</span>; <span class="id" title="tactic">simpl</span>;<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">try</span> (<span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHHty</span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">try</span> (<span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHHty1</span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">try</span> (<span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHHty2</span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">try</span> (<span class="id" title="tactic">rewrite</span> <span class="id" title="var">IHHty3</span>);<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">try</span> (<span class="id" title="tactic">rewrite</span> (<a class="idref" href="Typechecking.html#TypecheckerExtensions.eqb_ty_refl"><span class="id" title="lemma">eqb_ty_refl</span></a> <span class="id" title="var">T<sub>0</sub></span>));<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">try</span> (<span class="id" title="tactic">rewrite</span> (<a class="idref" href="Typechecking.html#TypecheckerExtensions.eqb_ty_refl"><span class="id" title="lemma">eqb_ty_refl</span></a> <span class="id" title="var">T<sub>1</sub></span>));<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">try</span> (<span class="id" title="tactic">rewrite</span> (<a class="idref" href="Typechecking.html#TypecheckerExtensions.eqb_ty_refl"><span class="id" title="lemma">eqb_ty_refl</span></a> <span class="id" title="var">T<sub>2</sub></span>));<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">try</span> (<span class="id" title="tactic">rewrite</span> (<a class="idref" href="Typechecking.html#TypecheckerExtensions.eqb_ty_refl"><span class="id" title="lemma">eqb_ty_refl</span></a> <span class="id" title="var">T<sub>3</sub></span>));<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">eauto</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;- <span class="id" title="tactic">destruct</span> (<span class="id" title="var">Gamma</span> <span class="id" title="var">x<sub>0</sub></span>); [<span class="id" title="tactic">assumption</span>| <span class="id" title="var">solve_by_invert</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">Admitted</span>. <span class="comment">(*&nbsp;...&nbsp;and&nbsp;delete&nbsp;this&nbsp;line&nbsp;*)</span><br/>
<span class="comment">(*&nbsp;<br/>
Qed.&nbsp;<span class="comment">(*&nbsp;...&nbsp;and&nbsp;uncomment&nbsp;this&nbsp;one&nbsp;*)</span><br/>
*)</span><br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Typechecking.html#TypecheckerExtensions"><span class="id" title="module">TypecheckerExtensions</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab364"></a><h4 class="section">Exercise: 5 stars, standard, optional (stlc_step_function)</h4>
 Above, we showed how to write a typechecking function and prove it
    sound and complete for the typing relation.  Do the same for the
    operational semantics -- i.e., write a <i>function</i> <span class="inlinecode"><span class="id" title="var">stepf</span></span> of type
    <span class="inlinecode"><span class="id" title="var">tm</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" title="var">option</span></span> <span class="inlinecode"><span class="id" title="var">tm</span></span> and prove that it is sound and complete with
    respect to <span class="inlinecode"><span class="id" title="var">step</span></span> from chapter <a href="MoreStlc.html"><span class="inlineref">MoreStlc</span></a>. 
</div>
<div class="code">

<span class="id" title="keyword">Module</span> <a id="StepFunction" class="idref" href="#StepFunction"><span class="id" title="module">StepFunction</span></a>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">MoreStlc</span>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">STLCExtended</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Operational&nbsp;semantics&nbsp;as&nbsp;a&nbsp;Coq&nbsp;function.&nbsp;*)</span><br/>
<span class="id" title="keyword">Fixpoint</span> <a id="StepFunction.stepf" class="idref" href="#StepFunction.stepf"><span class="id" title="definition">stepf</span></a> (<a id="t:65" class="idref" href="#t:65"><span class="id" title="binder">t</span></a> : <a class="idref" href="MoreStlc.html#STLCExtended.tm"><span class="id" title="inductive">tm</span></a>) : <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#option"><span class="id" title="inductive">option</span></a> <a class="idref" href="MoreStlc.html#STLCExtended.tm"><span class="id" title="inductive">tm</span></a><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;REPLACE&nbsp;THIS&nbsp;LINE&nbsp;WITH&nbsp;":=&nbsp;_your_definition_&nbsp;."&nbsp;*)</span>. <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Soundness&nbsp;of&nbsp;<span class="inlinecode"><span class="id" title="var">stepf</span></span>.&nbsp;*)</span><br/>
<span class="id" title="keyword">Theorem</span> <a id="StepFunction.sound_stepf" class="idref" href="#StepFunction.sound_stepf"><span class="id" title="lemma">sound_stepf</span></a> : <span class="id" title="keyword">∀</span> <a id="t:67" class="idref" href="#t:67"><span class="id" title="binder">t</span></a> <a id="t':68" class="idref" href="#t':68"><span class="id" title="binder">t'</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Typechecking.html#StepFunction.stepf"><span class="id" title="axiom">stepf</span></a> <a class="idref" href="Typechecking.html#t:67"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Typechecking.html#t':68"><span class="id" title="variable">t'</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a>  <a class="idref" href="Typechecking.html#t:67"><span class="id" title="variable">t</span></a> <a class="idref" href="MoreStlc.html#STLCExtended.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Typechecking.html#t':68"><span class="id" title="variable">t'</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;Completeness&nbsp;of&nbsp;<span class="inlinecode"><span class="id" title="var">stepf</span></span>.&nbsp;*)</span><br/>
<span class="id" title="keyword">Theorem</span> <a id="StepFunction.complete_stepf" class="idref" href="#StepFunction.complete_stepf"><span class="id" title="lemma">complete_stepf</span></a> : <span class="id" title="keyword">∀</span> <a id="t:69" class="idref" href="#t:69"><span class="id" title="binder">t</span></a> <a id="t':70" class="idref" href="#t':70"><span class="id" title="binder">t'</span></a>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Typechecking.html#t:69"><span class="id" title="variable">t</span></a> <a class="idref" href="MoreStlc.html#STLCExtended.:::x_'--&gt;'_x"><span class="id" title="notation"><span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:6%;'><span style='letter-spacing:-.2em;'>-</span><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span></span></a> <a class="idref" href="Typechecking.html#t':70"><span class="id" title="variable">t'</span></a>  <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">→</span></a>  <a class="idref" href="Typechecking.html#StepFunction.stepf"><span class="id" title="axiom">stepf</span></a> <a class="idref" href="Typechecking.html#t:69"><span class="id" title="variable">t</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="http://coq.inria.fr/library//Coq.Init.Datatypes.html#Some"><span class="id" title="constructor">Some</span></a> <a class="idref" href="Typechecking.html#t':70"><span class="id" title="variable">t'</span></a>.<br/>
<span class="id" title="keyword">Proof</span>. <span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span> <span class="id" title="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" title="keyword">End</span> <a class="idref" href="Typechecking.html#StepFunction"><span class="id" title="module">StepFunction</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="doc"> 
<div class="paragraph"> </div>

<a id="lab365"></a><h4 class="section">Exercise: 5 stars, standard, optional (stlc_impl)</h4>
 Using the Imp parser described in the <a href="https://softwarefoundations.cis.upenn.edu/lf-current/ImpParser.html"><span class="inlineref">ImpParser</span></a> chapter
    of <i>Logical Foundations</i> as a guide, build a parser for extended
    STLC programs.  Combine it with the typechecking and stepping
    functions from the above exercises to yield a complete typechecker
    and interpreter for this language. 
</div>
<div class="code">

<span class="id" title="keyword">Module</span> <a id="StlcImpl" class="idref" href="#StlcImpl"><span class="id" title="module">StlcImpl</span></a>.<br/>
<span class="id" title="keyword">Import</span> <span class="id" title="var">StepFunction</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;FILL&nbsp;IN&nbsp;HERE&nbsp;*)</span><br/>
<span class="id" title="keyword">End</span> <a class="idref" href="Typechecking.html#StlcImpl"><span class="id" title="module">StlcImpl</span></a>.<br/>
<font size=-2>&#9744;</font>
</div>

<div class="code">

<span class="comment">(*&nbsp;2021-08-11&nbsp;15:11&nbsp;*)</span><br/>
</div>
</div>

<div id="footer">
<hr/><a href="coqindex.html">Index</a><hr/>This page has been generated by <a href="http://coq.inria.fr/">coqdoc</a>
</div>

</div>

</body>
</html>